
%% bare_conf.tex
%% V1.3
%% 2007/01/11
%% by Michael Shell
%% See:
%% http://www.michaelshell.org/
%% for current contact information.
%%
%% This is a skeleton file demonstrating the use of IEEEtran.cls
%% (requires IEEEtran.cls version 1.7 or later) with an IEEE conference paper.
%%
%% Support sites:
%% http://www.michaelshell.org/tex/ieeetran/
%% http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/
%% and
%% http://www.ieee.org/

%%*************************************************************************
%% Legal Notice:
%% This code is offered as-is without any warranty either expressed or
%% implied; without even the implied warranty of MERCHANTABILITY or
%% FITNESS FOR A PARTICULAR PURPOSE! 
%% User assumes all risk.
%% In no event shall IEEE or any contributor to this code be liable for
%% any damages or losses, including, but not limited to, incidental,
%% consequential, or any other damages, resulting from the use or misuse
%% of any information contained here.
%%
%% All comments are the opinions of their respective authors and are not
%% necessarily endorsed by the IEEE.
%%
%% This work is distributed under the LaTeX Project Public License (LPPL)
%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used,
%% distributed and modified. A copy of the LPPL, version 1.3, is included
%% in the base LaTeX documentation of all distributions of LaTeX released
%% 2003/12/01 or later.
%% Retain all contribution notices and credits.
%% ** Modified files should be clearly indicated as such, including  **
%% ** renaming them and changing author support contact information. **
%%
%% File list of work: IEEEtran.cls, IEEEtran_HOWTO.pdf, bare_adv.tex,
%%                    bare_conf.tex, bare_jrnl.tex, bare_jrnl_compsoc.tex
%%*************************************************************************

% *** Authors should verify (and, if needed, correct) their LaTeX system  ***
% *** with the testflow diagnostic prior to trusting their LaTeX platform ***
% *** with production work. IEEE's font choices can trigger bugs that do  ***
% *** not appear when using other class files.                            ***
% The testflow support page is at:
% http://www.michaelshell.org/tex/testflow/



% Note that the a4paper option is mainly intended so that authors in
% countries using A4 can easily print to A4 and see how their papers will
% look in print - the typesetting of the document will not typically be
% affected with changes in paper size (but the bottom and side margins will).
% Use the testflow package mentioned above to verify correct handling of
% both paper sizes by the user's LaTeX system.
%
% Also note that the "draftcls" or "draftclsnofoot", not "draft", option
% should be used if it is desired that the figures are to be displayed in
% draft mode.
%
\documentclass[conference]{IEEEtran}
% Add the compsoc option for Computer Society conferences.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference]{../sty/IEEEtran}





% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)


% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional
% compilation based on whether the output is pdf or dvi.
% usage:
% \ifpdf
%   % pdf code
% \else
%   % dvi code
% \fi
% The latest version of ifpdf.sty can be obtained from:
% http://www.ctan.org/tex-archive/macros/latex/contrib/oberdiek/
% Also, note that IEEEtran.cls V1.7 and later provides a builtin
% \ifCLASSINFOpdf conditional that works the same way.
% When switching from latex to pdflatex and vice-versa, the compiler may
% have to be run twice to clear warning/error messages.






% *** CITATION PACKAGES ***
%
%\usepackage{cite}
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of IEEE. Loading the cite package will
% result in citation numbers being automatically sorted and properly
% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using
% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's
% \cite will automatically add leading space, if needed. Use cite.sty's
% noadjust option (cite.sty V3.8 and later) if you want to turn this off.
% cite.sty is already installed on most LaTeX systems. Be sure and use
% version 4.0 (2003-05-27) and later if using hyperref.sty. cite.sty does
% not currently provide for hyperlinked citations.
% The latest version can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/cite/
% The documentation is contained in the cite.sty file itself.






% *** GRAPHICS RELATED PACKAGES ***
%
\ifCLASSINFOpdf
  % \usepackage[pdftex]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../pdf/}{../jpeg/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.pdf,.jpeg,.png}
\else
  % or other class option (dvipsone, dvipdf, if not using dvips). graphicx
  % will default to the driver specified in the system graphics.cfg if no
  % driver is specified.
  % \usepackage[dvips]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../eps/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.eps}
\fi
% graphicx was written by David Carlisle and Sebastian Rahtz. It is
% required if you want graphics, photos, etc. graphicx.sty is already
% installed on most LaTeX systems. The latest version and documentation can
% be obtained at: 
% http://www.ctan.org/tex-archive/macros/latex/required/graphics/
% Another good source of documentation is "Using Imported Graphics in
% LaTeX2e" by Keith Reckdahl which can be found as epslatex.ps or
% epslatex.pdf at: http://www.ctan.org/tex-archive/info/
%
% latex, and pdflatex in dvi mode, support graphics in encapsulated
% postscript (.eps) format. pdflatex in pdf mode supports graphics
% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure
% that all non-photo figures use a vector format (.eps, .pdf, .mps) and
% not a bitmapped formats (.jpeg, .png). IEEE frowns on bitmapped formats
% which can result in "jaggedy"/blurry rendering of lines and letters as
% well as large increases in file sizes.
%
% You can find documentation about the pdfTeX application at:
% http://www.tug.org/applications/pdftex





% *** MATH PACKAGES ***
%
%\usepackage[cmex10]{amsmath}
% A popular package from the American Mathematical Society that provides
% many useful and powerful commands for dealing with mathematics. If using
% it, be sure to load this package with the cmex10 option to ensure that
% only type 1 fonts will utilized at all point sizes. Without this option,
% it is possible that some math symbols, particularly those within
% footnotes, will be rendered in bitmap form which will result in a
% document that can not be IEEE Xplore compliant!
%
% Also, note that the amsmath package sets \interdisplaylinepenalty to 10000
% thus preventing page breaks from occurring within multiline equations. Use:
%\interdisplaylinepenalty=2500
% after loading amsmath to restore such page breaks as IEEEtran.cls normally
% does. amsmath.sty is already installed on most LaTeX systems. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/





% *** SPECIALIZED LIST PACKAGES ***
%
%\usepackage{algorithmic}
% algorithmic.sty was written by Peter Williams and Rogerio Brito.
% This package provides an algorithmic environment fo describing algorithms.
% You can use the algorithmic environment in-text or within a figure
% environment to provide for a floating algorithm. Do NOT use the algorithm
% floating environment provided by algorithm.sty (by the same authors) or
% algorithm2e.sty (by Christophe Fiorio) as IEEE does not use dedicated
% algorithm float types and packages that provide these will not provide
% correct IEEE style captions. The latest version and documentation of
% algorithmic.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithms/
% There is also a support site at:
% http://algorithms.berlios.de/index.html
% Also of interest may be the (relatively newer and more customizable)
% algorithmicx.sty package by Szasz Janos:
% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithmicx/

\usepackage{listings}


\lstdefinelanguage{scala}{% 
       morekeywords={% 
                try, catch, throw, private, public, protected, import, package, implicit, final, package, trait, type, class, val, def, var, if, this, else, extends, with, while, new, abstract, object, requires, case, match, sealed,override},% 
         sensitive=t, % 
   morecomment=[s]{/*}{*/},morecomment=[l]{\//},% 
   escapeinside={/*\%}{*/},%
   rangeprefix= /*< ,rangesuffix= >*/,%
   morestring=[d]{"}% 
 }
 
\lstdefinelanguage{Haskell}{%
   otherkeywords={=>},%
   morekeywords={abstype,break,class,case,data,deriving,do,else,if,instance,newtype,of,return,then,where},%
   sensitive,%
   morecomment=[l]--,%
   morecomment=[n]{\{-}{-\}},%
   morestring=[b]"%
  }
  
%  numberbychapter=false,
\lstset{breaklines=true,language=scala} 
%\lstset{basicstyle=\footnotesize\ttfamily, breaklines=true, language=scala, tabsize=2, columns=fixed, mathescape=false,includerangemarker=false}
% thank you, Burak 
% (lstset tweaking stolen from
% http://lampsvn.epfl.ch/svn-repos/scala/scala/branches/typestate/docs/tstate-report/datasway.tex)
\lstset{
    xleftmargin=1em,%
    frame=single,%  TODO REMOVE only for floating listings
    captionpos=b,%
    fontadjust=true,%
    columns=[c]fixed,%
    keepspaces=true,%
    basewidth={0.56em, 0.52em},%
    tabsize=2,%
    basicstyle=\renewcommand{\baselinestretch}{0.97}\small\tt,% \small\tt
    commentstyle=\textit,%
    keywordstyle=\bfseries,%
}



% *** ALIGNMENT PACKAGES ***
%
%\usepackage{array}
% Frank Mittelbach's and David Carlisle's array.sty patches and improves
% the standard LaTeX2e array and tabular environments to provide better
% appearance and additional user controls. As the default LaTeX2e table
% generation code is lacking to the point of almost being broken with
% respect to the quality of the end results, all users are strongly
% advised to use an enhanced (at the very least that provided by array.sty)
% set of table tools. array.sty is already installed on most systems. The
% latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/required/tools/


%\usepackage{mdwmath}
%\usepackage{mdwtab}
% Also highly recommended is Mark Wooding's extremely powerful MDW tools,
% especially mdwmath.sty and mdwtab.sty which are used to format equations
% and tables, respectively. The MDWtools set is already installed on most
% LaTeX systems. The lastest version and documentation is available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/mdwtools/


% IEEEtran contains the IEEEeqnarray family of commands that can be used to
% generate multiline equations as well as matrices, tables, etc., of high
% quality.


%\usepackage{eqparbox}
% Also of notable interest is Scott Pakin's eqparbox package for creating
% (automatically sized) equal width boxes - aka "natural width parboxes".
% Available at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/eqparbox/





% *** SUBFIGURE PACKAGES ***
%\usepackage[tight,footnotesize]{subfigure}
% subfigure.sty was written by Steven Douglas Cochran. This package makes it
% easy to put subfigures in your figures. e.g., "Figure 1a and 1b". For IEEE
% work, it is a good idea to load it with the tight package option to reduce
% the amount of white space around the subfigures. subfigure.sty is already
% installed on most LaTeX systems. The latest version and documentation can
% be obtained at:
% http://www.ctan.org/tex-archive/obsolete/macros/latex/contrib/subfigure/
% subfigure.sty has been superceeded by subfig.sty.



%\usepackage[caption=false]{caption}
%\usepackage[font=footnotesize]{subfig}
% subfig.sty, also written by Steven Douglas Cochran, is the modern
% replacement for subfigure.sty. However, subfig.sty requires and
% automatically loads Axel Sommerfeldt's caption.sty which will override
% IEEEtran.cls handling of captions and this will result in nonIEEE style
% figure/table captions. To prevent this problem, be sure and preload
% caption.sty with its "caption=false" package option. This is will preserve
% IEEEtran.cls handing of captions. Version 1.3 (2005/06/28) and later 
% (recommended due to many improvements over 1.2) of subfig.sty supports
% the caption=false option directly:
%\usepackage[caption=false,font=footnotesize]{subfig}
%
% The latest version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/subfig/
% The latest version and documentation of caption.sty can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/caption/




% *** FLOAT PACKAGES ***
%
%\usepackage{fixltx2e}
% fixltx2e, the successor to the earlier fix2col.sty, was written by
% Frank Mittelbach and David Carlisle. This package corrects a few problems
% in the LaTeX2e kernel, the most notable of which is that in current
% LaTeX2e releases, the ordering of single and double column floats is not
% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a
% single column figure to be placed prior to an earlier double column
% figure. The latest version and documentation can be found at:
% http://www.ctan.org/tex-archive/macros/latex/base/



%\usepackage{stfloats}
% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e
% the ability to do double column floats at the bottom of the page as well
% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in
% LaTeX2e). It also provides a command:
%\fnbelowfloat
% to enable the placement of footnotes below bottom floats (the standard
% LaTeX2e kernel puts them above bottom floats). This is an invasive package
% which rewrites many portions of the LaTeX2e float routines. It may not work
% with other packages that modify the LaTeX2e float routines. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/sttools/
% Documentation is contained in the stfloats.sty comments as well as in the
% presfull.pdf file. Do not use the stfloats baselinefloat ability as IEEE
% does not allow \baselineskip to stretch. Authors submitting work to the
% IEEE should note that IEEE rarely uses double column equations and
% that authors should try to avoid such use. Do not be tempted to use the
% cuted.sty or midfloat.sty packages (also by Sigitas Tolusis) as IEEE does
% not format its papers in such ways.





% *** PDF, URL AND HYPERLINK PACKAGES ***
%
%\usepackage{url}
% url.sty was written by Donald Arseneau. It provides better support for
% handling and breaking URLs. url.sty is already installed on most LaTeX
% systems. The latest version can be obtained at:
% http://www.ctan.org/tex-archive/macros/latex/contrib/misc/
% Read the url.sty source comments for usage information. Basically,
% \url{my_url_here}.





% *** Do not adjust lengths that control margins, column widths, etc. ***
% *** Do not use packages that alter fonts (such as pslatex).         ***
% There should be no need to do such things with IEEEtran.cls V1.6 and later.
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )


% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}


\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired
\title{Bare Demo of IEEEtran.cls for Conferences}


% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{\IEEEauthorblockN{Michael Shell}
\IEEEauthorblockA{School of Electrical and\\Computer Engineering\\
Georgia Institute of Technology\\
Atlanta, Georgia 30332--0250\\
Email: http://www.michaelshell.org/contact.html}
\and
\IEEEauthorblockN{Homer Simpson}
\IEEEauthorblockA{Twentieth Century Fox\\
Springfield, USA\\
Email: homer@thesimpsons.com}
\and
\IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
\IEEEauthorblockA{Starfleet Academy\\
San Francisco, California 96678-2391\\
Telephone: (800) 555--1212\\
Fax: (888) 555--1212}}

% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts
% after \documentclass

% for over three affiliations, or if they all won't fit within the width
% of the page, use this alternative format:
% 
%\author{\IEEEauthorblockN{Michael Shell\IEEEauthorrefmark{1},
%Homer Simpson\IEEEauthorrefmark{2},
%James Kirk\IEEEauthorrefmark{3}, 
%Montgomery Scott\IEEEauthorrefmark{3} and
%Eldon Tyrell\IEEEauthorrefmark{4}}
%\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Electrical and Computer Engineering\\
%Georgia Institute of Technology,
%Atlanta, Georgia 30332--0250\\ Email: see http://www.michaelshell.org/contact.html}
%\IEEEauthorblockA{\IEEEauthorrefmark{2}Twentieth Century Fox, Springfield, USA\\
%Email: homer@thesimpsons.com}
%\IEEEauthorblockA{\IEEEauthorrefmark{3}Starfleet Academy, San Francisco, California 96678-2391\\
%Telephone: (800) 555--1212, Fax: (888) 555--1212}
%\IEEEauthorblockA{\IEEEauthorrefmark{4}Tyrell Inc., 123 Replicant Street, Los Angeles, California 90210--4321}}




% use for special paper notices
%\IEEEspecialpapernotice{(Invited Paper)}




% make the title area
\maketitle


\begin{abstract}
%\boldmath
The abstract goes here.
\end{abstract}
% IEEEtran.cls defaults to using nonbold math in the Abstract.
% This preserves the distinction between vectors and scalars. However,
% if the conference you are submitting to favors bold math in the abstract,
% then you can use LaTeX's standard command \boldmath at the very start
% of the abstract to achieve this. Many IEEE journals/conferences frown on
% math in the abstract anyway.

% no keywords




% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle



\section{Introduction}
% no \IEEEPARstart
This demo file is intended to serve as a ``starter file''
for IEEE conference papers produced under \LaTeX\ using
IEEEtran.cls version 1.7 and later.
% You must have at least 2 lines in the paragraph with the drop letter
% (should never be an issue)
I wish you the best of success.

\hfill mds
 
\hfill January 11, 2007

\section{casestudy: scrap your nameplate}

\subsection{structure of System F}
Whereas in the simply typed lambda calculus, we only had normal functions, that
is abstractions of a term over another term, with the variable term's type
annotated; System F allows type abstraction. Thus we can abstract a term over a
type in a polymorphic function. The type of such a type-abstracted term is no
longer a base type, but a type abstracted over another type. This can be either
universal abstraction where the type will then be of the form 'forall a . T', or
existential abstraction where the type hase the form 'exist a  . T' While
universal abstractions can model ordinary colection-type type abstraction,
existential abstraction models abstract data type or a module system.
\\

To implement this, it is obvious
we now get abstractions over terms and abstractions over types. When performing
substitution, we can now need to substitute a term into a term, a type into a
term, or a type into a type.

\subsection{nominal abstract syntax}
The scrap your nameplate approach is a library to deal with naming and
substitution in haskell. The big problem with
substitution in function abstractions is performing capture avoiding substitution.
There exist multiple mechanisms for dealing with name binding, proper capture
avoiding substitution and alpha-equivalence of expressions.
First order abstract syntax with explicit substitution boilerplate; name-free
such as debruijn indices or levels; higher-order abstract syntax which reuses
variables and bindings in the meta language.
\\
An alternative is nominal abstract syntax, named by
Cheney\citep{cheney-2005-36}, based on principles by Gabbay and Pitts. This introduces names as a seperate first class
entity and bindings as a datatype encapsulating the binding name and an expression under scope. The insight behind nominal
abstract syntax is the use of swapping of names instead of substitution of
one name for another as a mechanism of renaming. Swapping or invertible
renaming preserves
equality, disequality of names and freshness(not being used as a free variable)
in expressions. Ordinary renaming preserves equality (if t==u; 
$t[x:=y] == u[x:=y]$ ), but not inequality ( if x != y; x[x:=y] == y == y[x:=y]) or freshness
( x is not free in $\lambda$ x . f x y; but x[x:=y] == x is free in ($\lambda$
x. f x y)[x:=y] == ($\lambda$ x1 . f x1 y)). However, swapping two names
preserves these properties.
\\

For nominal abstract syntax, we need several concepts:
firstly names, optionally
subdivided in different nameclasses. Secondly, a swapping operation on
expressions, taking two names of the same type and swapping each for the other
everywhere in the expression. Thirdly a freshnes relation that determines
whether a name is fresh = non-free within a value. Fourthly a name-binder that
binds a name within a value and for which equality is alpha-equivalence.
Fifthly, a name generation mechanism that can always find a new fresh name,
globally or for a set of values. Then we need to reason with a number of rules:
governing the result of name swappings on names and bindings
%layout swapping rules for names and bindings%.
Also we define how the freshness relation between a name and a value is
calculated structurally. Here we use a structural building of the list of free
variables occurring within an expression, also known as its `support'. Finally
we define alpha-equivalence on these structures.

Based on these operations, defining substitution is easy: substitution on a
variable is trivial ( var(a)[a:=T] == T; var(b)[a:=T]== var(b)), substitution
on a binding somewhat less ( (<b>B)[a:=T] == <b> B' if a free in B and B[a:=T]
== B') but still a straightforward transcription of the original Barendregt
statement of capture-free substitution. Substitution on all other structures
just propagates to the structure's substructures.
\\

The original use of this naming system was as an extension to ML called
FreshML, later ported to haskell. Here abstractions are considered equal up to
alpha-renaming, and freshening occurs automatically during pattern matching of
an abstraction.

A disadvantage of using this naming system is that a lot of boilerplate code
has to be written. The definitions of the nominable operations and of
substitution may be trivial, but they are not built-in.

\subsection{overview of scrap your nameplate in haskell}
 FreshLib by Cheney used
generic programming to add nominal abstract syntax as a library to haskell. 
Cheney introduces a type class Nominal which contains the swap, fresh and
support functions. This type class is made derivable using any implementation
of derivable type classes. The user can then just append a deriving Nominal
clause to the definition of his abstract syntax tree data structure and get
these instances without further boilerplate.


The substitution function is implemented through the SYB3 method.


We have attempted to port this approach to Scala.




\subsection{Nominal in scala}
There is no system for derivable type classes yet in Scala. But we can layer
the definition of Nominal onto the generic spine view from Scrap your
boilerplate Revolutions.


First we define the general trait Nominal in Scala.

\begin{lstlisting}
trait Nominal[Self] {
  //def self:Self
  def swap(a: Name, b: Name): Self
  def fresh(a: Name): Boolean
  def supp: List[Name]
}

\end{lstlisting}
There are only two necessary special cases for nominal: names and bindings get a
predefined behaviour in the library. 

\begin{lstlisting}
class Name(val name: String) extends Nominal[Name] {
  def swap(a: Name, b: Name) = if(this == a) b else if(this == b) a else this
  def fresh(a: Name) = this != a
  def supp = List(this)
}
class \\[T](binder: Name, body: T)(implicit val bodynom: T => Nominal[T]) extends Nominal[\\[T]] {
  def swap(a: Name, b: Name) = \\(binder swap(a, b), body swap(a, b)) // boilerplate
  def fresh(a: Name) = if(a == binder) true else body fresh (a)
  def supp = body.supp filter (_ != binder)        
}

\end{lstlisting}


We intent to have our abstract syntax tree nodes use an implementation of this
based on their spine view. Indeed, the computation of the three functions can
be seen as a folding using different combining functions of specific
dispatching on the subterms. We thus get a mutually recursive implementation.


Firstly, for each of the functionalities, a specific method that captures the
special cases of names and bindings and defaults to the generic case,
converting the term into its spine representation. 

Secondly, a generic
function that defines the empty case, and in the case of a further constructor
with arguments, calls itself recursively on the generic component, calls the
specific function just mentioned on the argument, and combines the two elements.


This combination concludes the definition of Nominal, and a instance of Nominal
for a given type
\\
insert implementation
\\

Now, in our abstract syntax trees we want to use lambda abstractions
and universal types. Thus some of our nodes will contain a binding of a name in
a LTerm in the first case, and a binding of a name in a LType. The
implementation of bindings requires that the body is Nominal. Thus, we need to
make LTerm and LType nominal. There are two general ways to do this in Scala, 
externally or internally: using type class emulation with implicits, or using
inheritance.

If we intend to do it externally, we need an implicit instance of nominal for
LTerm and one for LType. This will be used as follows: a binding will call an
operation on its body of static type LTerm/LType. The implicit instance will be
put in between as a function that takes a LTerm/LType and 
gives back an nominal with the correct functions. We get a set of nominals for
each of the different LTerms by using the generic view on each
datatypeconstructor. In our implicit instance we will have to do the dispatch.
Thus we need one big pattern match over all terms, referring each to the right
derived nominal. 


Then to get the individual instances of nominal, we will have
a bunch of one-line nominal instances each generated by a function that
generates a nominal based on the generic view of a case class. Each of these instances
calls the function with as type parameters the type of the actual node, not the
supertype LTerm or LType. 
This nominal generating function takes the spine structure of a value of the
given node type. Thus also we once need to instantiate an implicit value to
 spine function for each nodetype. Again this is a set of one-line declarations.
 However, when converting a value of a specific node type to its spine
 representation, we need embed the spine instances for each of its parameters.
 Since these are often generally LTerm or LType, we additionally need to write
 a dispatching pattern matching type reification.
 
 
 Thus instead of the code for nominal in each nodetype, we need a dispatcher
 for nominal for LTerms and one for LTypes. The individual instances these
 dispatch to is a set of one-line boilerplate lines. \\
 Then the implementation
 of these function needs a generic view. This is boilerplate in common for the
 whole program, no matter how many generic functions are used. This also needs
 two dispatching functions and a set of one-line boilerplate lines.
 \\
 \\
 An alternative option is to use inheritance, and use the built-in dynamic
 dispatch instead of implementing it ourself.
 \\
 Now in both LTerm and LType, we declare that they implement Nominal. For
 primitive values, there is an easy dummy implementation for nominal we can just
 mix in as a trait in an intermediate abstract class BaseTerm and BaseType.
 For the general nodes, we can also create an intermediate abstract class
 GenericallyNominalTerm and GenericallyNominalType. What we want for each of
 the nodes inheriting from these intermediate classes, is to have the three
 functions of nominal implemented in the correct node-specific way. We thus
 redirect them to a local implementation of Nominal for the specific nodetype.
 
 
 \begin{lstlisting}[float=*tbph]
   //use to layer nominal on spineview
  class GenNominal[Self]( val self:Self)(implicit val tyman:TypeMan[Self]) extends Nominal[Self]{
    assume (tyman != null, "creating gennominal with tyman null: "+self)
    def swap(a: Name, b: Name): Self = (swapnames_gen(tyman.toValSpine(self))(a,b)).buildFromSpine
    def fresh(a: Name):Boolean  = freshname_gen(tyman.toValSpine(self))(a)
    def supp: List[Name] = suppnames_gen(tyman.toValSpine(self))
  }

  trait GenNominalByProxy[TermType, Self<: TermType] extends Nominal[TermType] {this: Self =>
    //input
    //this lazy val should override the def above, which ideally would be an abstract lazy val, but that's not possible
    //collapsed hierarchy to enable lazy val
    lazy val nomproxy:Nominal[Self] = {assume (( typeman != null), "generating nomproxy with typeman null for "+this)
      new GenNominal[Self](this)(typeman) {}
    }
    def swap(a:Name,b:Name):TermType = nomproxy.swap(a,b)
    def fresh(a:Name) = nomproxy.fresh(a)
    def supp = nomproxy.supp

    //how do we get typeman inserted early enough? skip doing it implicitly for now, just let implementing nodes make the link explicitly
    val typeman:TypeMan[Self]
  }
  

  def freshname[T](a:Name)(t:T)(implicit tman: TypeMan[T]):Boolean = t match {
    case trumps: Nominal[T] => trumps.fresh(a)
    case _ => {new Exception("Applying workfunctiondispatch on illegal type: trying spineview impl").printStackTrace();
      freshname_gen(tman.toValSpine(t))(a)}
  }
  def freshname_gen[T](ts:ValSpine[T])(a:Name):Boolean = ts match {
      case ConstrExt(_,_) => true
      case Apped(deep,Typed(arg,tman))=> freshname(a)(arg)(tman) && freshname_gen(deep)(a)
  }
  
  
  //all lterms should be nominal
  sealed abstract class LTerm extends Node with Nominal[LTerm]{this: (LTerm with Node) with Nominal[LTerm] =>
  }
  //in the non-base cases, we will derive the implementation from the TypeMan instance 
  sealed abstract class GenericallyTypeParamNominalLTerm[Self <:LTerm]
  extends LTerm with GenNominalByProxy[LTerm, Self] {this:Self => 
  //needs to be provided in subclass
  //val typeman:TypeMan[Self]
  }
  //for each subclass we extend the in-between class instead of LTerm itself
  //and provide the reference to the proper spinegenerator
  case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends GenericallyTypeParamNominalLTerm[If]{
    val typeman = IfTypeMan
  }
 
 
\end{lstlisting}
 
 With this approach, the boilerplate to provide the spine instances remains the
 same, but the additional boilerplate for the generation of nominal is a lot
 less. No dispatcher is needed, all the user needs to do is link to
 the correct spineprovider in each nodetype, and based thereon a generical
 nominal implementation will be derived.
 %Ideally we would want this implementating generated once for each nodetype.
 %To do this, we need a companion object for each nodetype that contains the
 %derived nominal implementation for that nodetype. So we still need to do a
 %part of the dispatch ourself, by having again a single line of boilerplate per
 %node.
 



\subsection{substitution in Scala}
The structure of substitution is different from that of nominality. 
For Nominal, the base cases, the special cases for the inductive definition 
are only names and binders that are provided in the library. The implementation 
for all other datatypes depends purely on
distribution through the structural view up unto those base cases.
However, in defining
substitution the base cases are no longer just binders and names. The user-defined 
datatype signifying a variable reference, which contains a name, needs special 
treatment. Not the inner name is to be swapped, but the referencing node 
itself is substituted by a part of a tree. The
other base case is again the binding form in the library.
\\

The first problem arises because we have bindings for multiple sorts of nodes.
In system f a type can not depend an a value, so our LType nodes contain only
types. Therefore, a LType node cannot contain references to term variables, only to type
variables. So a type variable substitution on LTypes needs to be propagated, while the result of 
any term variable substitution is simply the original LType node itself. In the
implementation the interface to the substitution functionality provided to the
typechecking and evaluation modules does not even expose a function to perform
it.




However, our LTerm nodes can contain further terms, but also types. Thus LTerms
need to be substitutable with both type variable substitutions and term
variable substitutions. Ideally we could just let it implement a trait
'TakesParam' once with type parameter LTerm and once with type parameter LType.
However, Scala does not allow a given class to implement the same trait twice
with different type parameters. During the implementation of nominal it was
clear that using inheritance for dispatching is cleaner and shorter than using
type classes and simulating the dispath ourself. This inheritance route is not
possible here.
\\

Still, a conceptual view on how it could be implemented is useful.
The abstract class LType would extend the substable[LType] trait. Again, a
subclass GenericSubstableLType would mix in a GenericSubstable[LType]
implementation. All ltypes except TyVar would extend this, while TyVar would
get its own specific library-provided ContainsName\_Substable[LType]
implementation mixed in.

LTerm on the other hand would mix in both Substable[LType] and Substable[LTerm].
Again almost all subclasses would use a generic implementation, while Var
would mix in ContainsName\_Substable[LTerm] and ContainsNameOfOtherType[LType].
This last is possible to signify that while we have a single Name class, we
still know based on the type of the substitution whether it can possible match
or not.
\\

A first implementation technique that can be implemented is simply using an
external function. This will catch special cases, redirect the scope and variable cases
to the appropriate methods and generically iterate in the default case.

The most complex case, of inserting a type substitution into any :
First we check manually if this is an exception by using a partialFunction. If
so, we jump to the exceptional behaviour, passing the method itself in case the
exeption needs to perform a recursive call.
This takes a lot of code, which can be shrunk by using the right combinators.
Afterwards we take on the two library cases: binding scopes and variables.
Unfortunately, type erasure semantics in scala conspire to conflate both of the
binding scope cases, even though we need to distinguish between them to pass
the correct witness. We can however do this at runtime using a try-catch block.
The upcoming Manifest support can help here too once it implements a correct
non-erased subtype relation.

Finally we come to the general cases that cover all nodes not in the exception
clause.

\begin{lstlisting}[float=*tbph]

object typeintoany_scope {
  def exceptionLTerm(sub:substitution[LType],recself:Function2[substitution[LType],LTerm,LTerm]):PartialFunction[LTerm,LTerm] = {
    case r@Record(fields) => 
      Record(fields.map( {case (lbl,term) => (lbl, recself(sub,term))})).asInstanceOf[LTerm]  }
  def exceptionLTermLifted[T](sub:substitution[LType],recself:Function2[substitution[LType],LTerm,LTerm]):PartialFunction[T,T] = 
    new PartialFunction[T,T] {
      def apply(t:T) = t match {case lt:LTerm => exceptionLTerm(sub,recself).apply(lt).asInstanceOf[T]}
      def isDefinedAt(t:T):Boolean = t match {case lt:LTerm => exceptionLTerm(sub,recself).isDefinedAt(lt); case _ => false}
  }
  def exceptionLType(sub:substitution[LType],recself:Function2[substitution[LType],LType,LType]):PartialFunction[LType,LType] = {
    case TyRecord(fields) => {
        TyRecord(fields.map( {case (l,ty) => (l, ty subst (sub) )}))
  }}
  def exceptionLTypeLifted[T](sub:substitution[LType],recself:Function2[substitution[LType],LType,LType]):PartialFunction[T,T] = 
      new PartialFunction[T,T] {
        def apply(t:T) = t match {case lt:LType => exceptionLType(sub,recself).apply(lt).asInstanceOf[T]}
        def isDefinedAt(t:T):Boolean = t match {case lt:LType => exceptionLType(sub,recself).isDefinedAt(lt); case _ => false}
      }

  def specificSubstituteWithLType[T](sub: substitution[LType], t:T)(implicit tman:TypeMan[T],termman:TypeMan[LTerm],tyman:TypeMan[LType]):T = {
        //first any exceptions
        val excclauses = exceptionLTermLifted[T](sub,specificSubstituteWithLType[LTerm] _);
        if (excclauses.isDefinedAt(t)) {println("taking exception for "+t);excclauses(t)}
        else{
        val excclauses2 = exceptionLTypeLifted[T](sub,specificSubstituteWithLType[LType] _);
        if (excclauses2.isDefinedAt(t)) excclauses2(t)
        else
        
      t match {
        //then we get the two libraryprovided cases
        //this case should work on trait HasName
        //not just a type inference bug causing cast
        case dis @TyVar(n) =>sub(n).getOrElse[LType](dis).asInstanceOf[T] //will never be the same name
        //      type inference finds \\[LTerm], needs T
        //erasure problem: will also take a binds[LTerm], cannot take distinguish, and one branch will throw classcastexception
        //case body:Binds[LTerm] => (new AbsSubstTo[LType]).AbsIsSubstable(body)(LTermTakesLTypeParam).subst(sub).asInstanceOf[T]
        //case body:Binds[LType] => (new AbsSubstTo[LType]).AbsIsSubstable(body)(LTypeTakesLTypeParam).subst(sub).asInstanceOf[T]
        case body:Binds[LTerm] =>  try {
          (new AbsSubstTo[LType]).AbsIsSubstable(body)(LTermTakesLTypeParam).subst(sub).asInstanceOf[T]
        } catch { case e:ClassCastException =>  t match{
          case body:Binds[LType] => (new AbsSubstTo[LType]).AbsIsSubstable(body)(LTypeTakesLTypeParam).subst(sub).asInstanceOf[T] }
        }
        
    //then the redirect to the general cases
    //identified T with LTerm, but still needs cast!
    
    case term:LTerm => { 
      GenericLTypeIntoTSubst[LTerm](termman.toValSpine(term),sub).buildFromSpine.asInstanceOf[T] }
    case typ:LType => {
      GenericLTypeIntoTSubst[LType](tyman.toValSpine(typ),sub).buildFromSpine.asInstanceOf[T]  }
    
    case other     => GenericLTypeIntoTSubst(tman.toValSpine(other),sub).buildFromSpine
    
  }}
  }
  
  def GenericLTypeIntoTSubst[T](vs:ValSpine[T], sub: substitution[LType]):ValSpine[T] = vs match{
  case c@ConstrExt(_,_) => c
  case Apped(deep,Typed(arg,argtman)) => { val argmod = specificSubstituteWithLType(sub,arg)(argtman,TypeManDefs.LTermTypeMan,TypeManDefs.LTypeTypeMan)
    Apped(GenericLTypeIntoTSubst(deep,sub), Typed(argmod,argtman)) }
  }
} 

\end{lstlisting}




This approach requires that everyone using the library extends it by using its
substitution components to write his own substitution function. By introducing
the combinators from the original SYB paper, we can modularize this a bit more.




TODO: insert version with Excepting


\subsection{Using type manifests}


TODO: insert inverted typeman system

\subsubsection{rendered in scala}
\subsubsection{problems/modifications}
One of the major differences one runs into is between adts in haskell and case
class hierarchies in scala. The effect of an adt in haskell in like having a
name for the type Either<caseclass1,Either<caseclass2,\ldots
Because the top name is a type too, we need to implement dispatchers.






\newpage
\subsection{comparison debruijn/nomabss/scrapped}
In general it is possible to get the advantages of datatype-generic programming
in Scala. However the fixed overhead per datatype is greater than in haskell.
So while the code is more general and will adapt itself to new types, it takes
more generic code before the code will be shorter than the manual program. 
\subsubsection{modifiability, verbosity,..}




% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
% For figures, \caption should occur after the \includegraphics.
% Note that IEEEtran v1.7 and later has special internal code that
% is designed to preserve the operation of \label within \caption
% even when the captionsoff option is in effect. However, because
% of issues like this, it may be the safest practice to put all your
% \label just after \caption rather than within \caption{}.
%
% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class
% option should be used if it is desired that the figures are to be
% displayed while in draft mode.
%
%\begin{figure}[!t]
%\centering
%\includegraphics[width=2.5in]{myfigure}
% where an .eps filename suffix will be assumed under latex, 
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
%\caption{Simulation Results}
%\label{fig_sim}
%\end{figure}

% Note that IEEE typically puts floats only at the top, even when this
% results in a large percentage of a column being occupied by floats.


% An example of a double column floating figure using two subfigures.
% (The subfig.sty package must be loaded for this to work.)
% The subfigure \label commands are set within each subfloat command, the
% \label for the overall figure must come after \caption.
% \hfil must be used as a separator to get equal spacing.
% The subfigure.sty package works much the same way, except \subfigure is
% used instead of \subfloat.
%
%\begin{figure*}[!t]
%\centerline{\subfloat[Case I]\includegraphics[width=2.5in]{subfigcase1}%
%\label{fig_first_case}}
%\hfil
%\subfloat[Case II]{\includegraphics[width=2.5in]{subfigcase2}%
%\label{fig_second_case}}}
%\caption{Simulation results}
%\label{fig_sim}
%\end{figure*}
%
% Note that often IEEE papers with subfigures do not employ subfigure
% captions (using the optional argument to \subfloat), but instead will
% reference/describe all of them (a), (b), etc., within the main caption.


% An example of a floating table. Note that, for IEEE style tables, the 
% \caption command should come BEFORE the table. Table text will default to
% \footnotesize as IEEE normally uses this smaller font for tables.
% The \label must come after \caption as always.
%
%\begin{table}[!t]
%% increase table row spacing, adjust to taste
%\renewcommand{\arraystretch}{1.3}
% if using array.sty, it might be a good idea to tweak the value of
% \extrarowheight as needed to properly center the text within the cells
%\caption{An Example of a Table}
%\label{table_example}
%\centering
%% Some packages, such as MDW tools, offer better commands for making tables
%% than the plain LaTeX2e tabular which is used here.
%\begin{tabular}{|c||c|}
%\hline
%One & Two\\
%\hline
%Three & Four\\
%\hline
%\end{tabular}
%\end{table}


% Note that IEEE does not put floats in the very first column - or typically
% anywhere on the first page for that matter. Also, in-text middle ("here")
% positioning is not used. Most IEEE journals/conferences use top floats
% exclusively. Note that, LaTeX2e, unlike IEEE journals/conferences, places
% footnotes above bottom floats. This can be corrected via the \fnbelowfloat
% command of the stfloats package.



\section{Conclusion}
The conclusion goes here.




% conference papers do not normally have an appendix


% use section* for acknowledgement
\section*{Acknowledgment}


The authors would like to thank...





% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}

% references section

% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
%\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)
\begin{thebibliography}{1}

\bibitem{IEEEhowto:kopka}
H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
  0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.

\end{thebibliography}




% that's all folks
\end{document}


